w:World, a, b:E. FairFifo  (w_locl(w;a;b)  (loc(a) = loc(b)  Id & a < b)) 

latex

Definitions

t  T, x:A. B(x), FairFifo, x:AB(x), E, e < e', x:A  B(x), P  Q, World, time(e), a < b, w-info(w;e), x.A(x), loc(e), Id, s = t, P & Q, w_locl(w;x;y), P  Q, , {x:A| B(x)} , Type, , w-pred(w;e), pred(e), first(e), b, A, A c B, rel_exp(T;R;n), f(a), , x:A. B(x), P  Q, x f y, R^+, (i = j), {T}, SQType(T), , s ~ t, #$n, left + right, P  Q, Dec(P), A  B, Void, False, <a, b>, b, , Unit, n - m, -n, n+m, loc(e), a(i;t), isnull(a), Atom$n, i  j , x. t(x), t.2, t.1

Lemmas

w locl wf, cless wf, w-cless-loc, pi1 wf, pi2 wf, rel exp add, ge wf, nat properties, w-pred-bound, w-loc-lemma, Id sq, w-isnull wf, w-a wf, decidable lt, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, w-loc-w-pred, w-pred-decreases, nat plus properties, le wf, decidable int equal, nat plus wf, rel exp wf, nat plus inc, not wf, assert wf, first wf, pred wf, w-pred wf, loc wf, Id wf, w-info wf, w-time wf, nat wf, world wf, w-E wf, fair-fifo wf